﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics;
using OpSatPlan.PlanningGraph;
using OpSatPlan.SatSolvers;
using OpSatPlan.Encoder;
using System.IO;

namespace OpSatPlan
{
    public class Planner
    {
        private Domain mDomain;
        private Problem mProblem;
        private SatSolver mSolver;

        public class Plan
        {
            List<List<Action>> mPlan;
            public Plan(int numSteps)
            {
                this.mPlan = new List<List<Action>>();
                for (int i = 0; i < numSteps; i++)
                {
                    this.mPlan.Add(new List<Action>());
                }
            }
            public void Add(Action a, int step)
            {
                this.mPlan[step].Add(a);
            }
            public override string ToString()
            {
                string plan = "";
                for (int i = 0; i < this.mPlan.Count; i++)
                {
                    foreach (Action a in this.mPlan[i])
                    {
                        plan += string.Format("\t{0}:{1}{2}", i, a, System.Environment.NewLine);
                    }
                }
                return plan;
            }
        }
        public class PlanStats
        {
            private int mNumberOfVariables;
            private int mNumberOfClauses;
            private decimal mEncodingTime;
            private decimal mSolvingTime;
            private int mNumberOfTimeSteps;
            private decimal mTotalTime;
            private Plan mPlan;
            public PlanStats(int numVars, int numClause, decimal encodeTime,
                                decimal solveTime, int numSteps)
            {
                this.mNumberOfVariables = numVars;
                this.mNumberOfClauses = numClause;
                this.mEncodingTime = encodeTime;
                this.mSolvingTime = solveTime;
                this.mNumberOfTimeSteps = numSteps;
                this.mTotalTime = this.mEncodingTime + this.mSolvingTime;
            }
            public Plan Plan
            {
                get { return this.mPlan; }
                set { this.mPlan = value; }
            }
            public int NumberOfVariables
            {
                get
                { return this.mNumberOfVariables; }
            }
            public int NumberOfClauses
            {
                get { return this.mNumberOfClauses; }
            }
            public decimal EncodingTime
            {
                get { return this.mEncodingTime; }
            }
            public decimal SolvingTime
            {
                get { return this.mSolvingTime; }
            }
            public int NumberOfTimeSteps
            {
                get { return this.mNumberOfTimeSteps; }
            }
            public decimal TotalTime
            {
                get { return this.mTotalTime; }
            }
            public override string ToString()
            {
                string text;

                text = new string('=', 79);
                text += System.Environment.NewLine;
                text += String.Format("Number of variables:\t\t\t{0}{1}", this.NumberOfVariables, System.Environment.NewLine);
                text += String.Format("Number of clauses:\t\t\t{0}{1}", this.NumberOfClauses, System.Environment.NewLine);
                text += String.Format("Number of time steps:\t\t\t{0}{1}", this.NumberOfTimeSteps, System.Environment.NewLine);
                text += String.Format("Encoding time:\t\t\t\t{0}{1}", this.EncodingTime, System.Environment.NewLine);
                text += String.Format("Solving time:\t\t\t\t{0}{1}", this.SolvingTime, System.Environment.NewLine);
                text += String.Format("Total time:\t\t\t\t{0}{1}", this.TotalTime, System.Environment.NewLine);
                text += new string('=', 79);
                return text;
            }
            public override bool Equals(object obj)
            {
                if (obj == null)
                    return false;
                else if (obj.GetType() == typeof(PlanStats))
                    return this == (PlanStats)obj;
                else
                    return false;
            }

            public static bool operator ==(PlanStats x, PlanStats y)
            {
                if (System.Object.ReferenceEquals(x, y))
                    return true;
                else if ((object)x == null || (object)y == null)
                    return false;
                else
                    return x.GetHashCode() == y.GetHashCode();

            }
            public static bool operator !=(PlanStats x, PlanStats y)
            {
                return !(x == y);
            }
            public override int GetHashCode()
            {
                return this.mNumberOfTimeSteps.GetHashCode();
            }
        }
        public Planner(Domain domain, Problem problem, SatSolver solver)
        {
            this.mDomain = domain;
            this.mProblem = problem;
            this.mSolver = solver;
        }

        public void Solve(Input input, Stopwatch stopwatch)
        {
            RelaxedPlanningGraph rpg;
            Level level;
            CnfEncoder encoder;
            List<PlanStats> statsList = new List<PlanStats>();
            
            rpg = new RelaxedPlanningGraph(this.mDomain, this.mProblem);

            level = rpg.GetLastLevel();

            Output.Write("Initiating planning graph");
            // propogate levels till goal state is reached

            if (input.NumberOfSteps != int.MaxValue)
            {
                while (rpg.TimeSteps < input.NumberOfSteps)
                {
                    level = rpg.AddLevel();
                }
                Output.Write("Graph extended to " + (rpg.TimeSteps) + " time steps");
                Output.Write(new String('=', 79));
            }
            else
            {
                while (!level.StateIsPresent(this.mProblem.GoalState))
                {
                    level = rpg.AddLevel();
                }
                Output.Write("Goal state found at " + (rpg.TimeSteps) + " time steps");
                Output.Write(new String('=', 79));
            }
            Output.Write("");
            // encode rpg into a sat instance and call solver.
            bool sat = false;
            bool?[] model = null;
            encoder = new CnfEncoder(rpg, input);

            long encodeTime;
            long solveTime;
            long startTime;
            PlanStats stats = null;
            int upperBound = (rpg.TimeSteps) * 2;
            int lowerBound = rpg.TimeSteps;
            List<int> timeStepAttempts = new List<int>();
            while (true)
            {
                if (timeStepAttempts.Contains(rpg.TimeSteps) || rpg.TimeSteps == 0)
                {
                    break;
                }
                timeStepAttempts.Add(rpg.TimeSteps);

                encoder.Reset();
                this.mSolver.Reset();

                Output.Write(new String('=', 79));
                Output.Write("Encoding for " + (rpg.TimeSteps) + " timesteps");

                startTime = stopwatch.ElapsedMilliseconds;
                // encode to cnf
                encoder.Encode();

                encodeTime = stopwatch.ElapsedMilliseconds - startTime;

                // used for debugging purposes, write out a file with the text
                bool writeFile = false;
                if (writeFile)
                {
                    HumanReadableEncoder hre = new HumanReadableEncoder(encoder);
                    hre.Encode();
                }
                if (!input.CnfOnly)
                {

                    Output.Write("Attempting to solve for " + (rpg.TimeSteps) + " time steps");

                    startTime = stopwatch.ElapsedMilliseconds;
                    // call sat solver
                    sat = this.mSolver.Solve((int)(input.TimeLimitMilliseconds - stopwatch.ElapsedMilliseconds), encoder.CnfFileName);
                    solveTime = stopwatch.ElapsedMilliseconds - startTime;

                    stats = new PlanStats(encoder.NumberOfVariables, encoder.NumberOfClauses, (decimal)(encodeTime / 1000.0),
                                            (decimal)(solveTime / 1000.0), rpg.Depth - 1);
                    if (!sat)
                    {
                        Output.Write("Instance Unsatisfiable");
                        Output.Write(stats.ToString());
                        lowerBound = rpg.TimeSteps;
                        int numToExtend = (int)Math.Ceiling((upperBound - rpg.TimeSteps) / 2.0);
                        if (numToExtend == 0)
                        {
                            upperBound = upperBound * 2;
                            numToExtend = (int)Math.Ceiling((upperBound - rpg.TimeSteps) / 2.0);
                        }
                        Output.Write("Extending Planning Graph " + numToExtend + " time steps");
                        for (int i = 0; i < numToExtend; i++)
                        {
                            level = rpg.AddLevel();
                        }
                    }
                    else
                    {
                        statsList.Add(stats);
                        Output.Write("Instance Satisfiable");
                        Output.Write(stats.ToString());
                        model = this.mSolver.Model;

                        Plan plan = encoder.GetPlan(model);
                        stats.Plan = plan;
                        upperBound = rpg.TimeSteps;
                        int numToReduce = (int)((upperBound - lowerBound) / 2.0);
                        Output.Write("Reducing Planning Graph " + numToReduce + " time steps");
                        for (int i = 0; i < numToReduce; i++)
                        {
                            rpg.RemoveLastLevel();
                        }
                    }
                }
                else
                {
                    break;
                }
            }

            if (!input.CnfOnly && System.IO.File.Exists(encoder.CnfFileName))
                System.IO.File.Delete(encoder.CnfFileName);
            if (!input.CnfOnly)
            {
                stats = statsList[statsList.Count - 1];
                Output.Write("");
                Output.Write("Instance Satisfiable -- Step Optimal Plan");
                Output.Write(stats.ToString());
                Output.Write(stats.Plan.ToString());
                Output.Write("");
            }
        }
    }
}
